Inference at * 1 1 2 
Iof proof for Lemma complete nat ind with y:



1. P : {k}
2. g : i:. (j:i. P(j))  P(i)
3. Y(f,x. g(x,f))  !Void()!Void()
  Y(f,x. g(x,f))  (i:. P(i)) 

latex

 by Assert n:. Y(f,x. g(x,f))  (m:n. P(m)) 

latex

 1: .....assertion..... NILNIL

 1:   n:. Y(f,x. g(x,f))  (m:n. P(m))
 2: 

 2: 4. n:. Y(f,x. g(x,f))  (m:n. P(m))
 2:   Y(f,x. g(x,f))  (i:. P(i))
 .

Definitions

, t  T, x:A. B(x), {i..j}, #$n, x(s), Y, x.A(x), f(a)